|
|
Verification of Programs with Pointers Based on Pattern Detection
Kubíček, Jan ; Erlebach, Pavel (referee) ; Vojnar, Tomáš (advisor)
This paper presents our results in study of verifiaction of infinite state space systems. We deal more concretely with abstract model checking. As main part of study we learned about pattern-based verification. This method is supposed to verify programs with dynamic memory structures like lists. Those structures are presented as directed graph. Pattern-based verifiaction abstracts any number of nodes by replacing them with summarized node. This way we achieve bounded presentation of unbounded memory structure. Afterwards, verification is very effective due to low number of possible memory configurations. In our own work we deal with making model of a program for a tool that implements pattern-based verification. This model isconstructed from a subset of the C language. The main contribution of work is making the verification of simple programs written in C language completely self-acting by automation of constructing input model. In this paper wepresent the grammar of created subset of the C language and implementation details of translation.
|
|
|
Automata in Decision Procedures and Performance Analysis
Fiedor, Tomáš ; Barnat, Jiří (referee) ; Radu, Iosif (referee) ; Vojnar, Tomáš (advisor)
Tato práce se věnuje vylepšení současného stavu formalní analýzy a verifikace založené na automatech a zaměřené na systémy s nekonečnými stavovými prostory. V první části se práce zabývá dvěma rozhodovacími procedurami pro logiku WS1S, které jsou založené na korespondenci mezi formulemi logiky WS1S a konečnými automaty. První metoda je založena na tzv. antiřetězcích, ale, je limitována pouze na formule v prenexním normálním tvaru. Následně je tento přístup zobecněn na libovolné formule, jsou zavedeny tzv. jazykové termy a na jejich základě je navržena nová procedura, která pracuje za běhu a zpracovává tyto termy "líným" způsobem. Abychom získali efektivní rozhodovací proceduru, je dále navržena sada optimalizací (přičemž některé nejsou limitovány pouze pro naše přístupy). Obě metody jsou srovnány s ostatními nástroji implementujícími různé známé rozhodovací procedury. Získané výsledky jsou povzbuzující a ukazují, že použitelnost logiky WS1S je možno rozšířit na širší třídu formulí. V druhé části se práce zabývá analýzou mezí zdrojů programů manipulujících s haldou. Je zde navržena nová třída tzv. tvarových norem založených na délkách cest mezi význačnými místy na haldě, které jsou automaticky odvozovány z analyzovaného programu. Na základě této třídy norem je dále navržen kalkul, který je schopen přesně odvodit změny odvozených normů a použít je k vygenerování odpovídající celočíselné reprezentace vstupního programu, která je následně využita pro následovanou dedikovanou analýzou mezí zdrojů. Tato metoda byla implementována nad analýzou tvaru založenou na tzv. lesních automatech, implementovanou v nástroji Forester, a dále byl použit dobře zavedený analyzátor mezí zdrojů, implementovaný v nástroji Loopus. V experimentální evaluaci bylo ukázáno, že je opravdu takto získán silný analyzátor, který je schopen odvodit meze programů, které ještě nikdy plně automatizovaně odvozené nebyly.
|
|
|
Automata in Decision Procedures and Performance Analysis
Fiedor, Tomáš ; Barnat, Jiří (referee) ; Radu, Iosif (referee) ; Vojnar, Tomáš (advisor)
Tato práce se věnuje vylepšení současného stavu formalní analýzy a verifikace založené na automatech a zaměřené na systémy s nekonečnými stavovými prostory. V první části se práce zabývá dvěma rozhodovacími procedurami pro logiku WS1S, které jsou založené na korespondenci mezi formulemi logiky WS1S a konečnými automaty. První metoda je založena na tzv. antiřetězcích, ale, je limitována pouze na formule v prenexním normálním tvaru. Následně je tento přístup zobecněn na libovolné formule, jsou zavedeny tzv. jazykové termy a na jejich základě je navržena nová procedura, která pracuje za běhu a zpracovává tyto termy "líným" způsobem. Abychom získali efektivní rozhodovací proceduru, je dále navržena sada optimalizací (přičemž některé nejsou limitovány pouze pro naše přístupy). Obě metody jsou srovnány s ostatními nástroji implementujícími různé známé rozhodovací procedury. Získané výsledky jsou povzbuzující a ukazují, že použitelnost logiky WS1S je možno rozšířit na širší třídu formulí. V druhé části se práce zabývá analýzou mezí zdrojů programů manipulujících s haldou. Je zde navržena nová třída tzv. tvarových norem založených na délkách cest mezi význačnými místy na haldě, které jsou automaticky odvozovány z analyzovaného programu. Na základě této třídy norem je dále navržen kalkul, který je schopen přesně odvodit změny odvozených normů a použít je k vygenerování odpovídající celočíselné reprezentace vstupního programu, která je následně využita pro následovanou dedikovanou analýzou mezí zdrojů. Tato metoda byla implementována nad analýzou tvaru založenou na tzv. lesních automatech, implementovanou v nástroji Forester, a dále byl použit dobře zavedený analyzátor mezí zdrojů, implementovaný v nástroji Loopus. V experimentální evaluaci bylo ukázáno, že je opravdu takto získán silný analyzátor, který je schopen odvodit meze programů, které ještě nikdy plně automatizovaně odvozené nebyly.
|
|
|
Verification of Programs with Pointers Based on Pattern Detection
Kubíček, Jan ; Erlebach, Pavel (referee) ; Vojnar, Tomáš (advisor)
This paper presents our results in study of verifiaction of infinite state space systems. We deal more concretely with abstract model checking. As main part of study we learned about pattern-based verification. This method is supposed to verify programs with dynamic memory structures like lists. Those structures are presented as directed graph. Pattern-based verifiaction abstracts any number of nodes by replacing them with summarized node. This way we achieve bounded presentation of unbounded memory structure. Afterwards, verification is very effective due to low number of possible memory configurations. In our own work we deal with making model of a program for a tool that implements pattern-based verification. This model isconstructed from a subset of the C language. The main contribution of work is making the verification of simple programs written in C language completely self-acting by automation of constructing input model. In this paper wepresent the grammar of created subset of the C language and implementation details of translation.
|
guest ::
